Exercise 2 --- ELG 7187C --- Winter 2007
(February 2, 2007, due date February 13)
We consider the protocol defined by the following diagram which contains
two state machines that communicate with one another. You may think of telephone
call establishment. On the left is the telephone (and the user) and the right
represents the central office of the telephone company. R means
ready, C means connected, Req means call request, Inc means incoming call
notification, and Term means termination of the call.
Part A: In this exercise, we propose to interpret these two diagrams in three different
manners:
- As two LTS that communicate by rendezvous for the three interactions
Req, Int and Term (that means, we ignore the + and - signs): Please consider
the composition of these two machines and indicate its behavior (in the form
of a single LTS), that means, do a reachability analysis (do you detect any
design error ? ). If you find a problem with the design, please suggest a
modification of the defined behavior for the machines in order to resolve
the identified problem. Please explain !
- As two IOA that communicate by direct coupling for the three interactions
Req, Int and Term (the - means output and + means input): Please consider the composition of
these two machines and indicate its behavior (in the form of a single state
machine), that means, do a reachability analysis (do you detect any design
error ? ). If you find a problem with the design, please suggest a modification
of the defined behavior for the machines in order to resolve the identified
problem. Please explain !
- As two communicating finite state machines that communicate by
message passing with queuing: Please consider the composition of
these two machines and indicate its behavior (in the form of a single transition
diagram), that means, do a reachability analysis (do you detect any design
error ? ) . If you find a problem with the design, please suggest a modification
of the defined behavior for the machines in order to resolve the identified
problem. If the reachable queue length is not bounded you will not be able
to perform a complete reachability analysis. Please explain !
Part B: Now we assume
that the specification of the left machine has been changed and an additional "- Term"
transition from state C back to state C is introduced (Note: This modified component is
non-deterministic). Do again the three tasks above.